$\forall$$A$, $C$:Type, ${\it eqa}$:EqDecider($A$), ${\it eqc}$:EqDecider($C$), ${\it eqc'}$:Top, $r$:($A$$\rightarrow$$C$), $f$:$a$:$A$ fp$\rightarrow$ Top, $a$:$A$.
\\[0ex]\{$a$ $\in$ dom($f$) $\Rightarrow$ $r$($a$) $\in$ dom(rename($r$;$f$))\}